package resolution;

import java.util.ArrayList;

import base.Atome;
import base.Formule;
import base.Non;


/**
 * Structure en arbre permettant de resoudre un systeme de preuve.
 * SI un  element n'a pas de pere c'est la racine
 * @author mathieu herbert
 *
 */
public class ArbreClause {

	/**
	 * Les fils
	 */
	ArrayList<ArbreClause> sousNoeud;
	/**
	 * La formule forme clausale: unification(une des autres  + noeud)
	 */
	ArrayList<Formule> formule;
	
	/**
	 * le pere du noeud
	 */
	public ArbreClause pere;
	
	/**
	 * premisses originale + ccl
	 */
	public ArrayList<ArrayList<Formule>> autres;
	
	////////////////////
	// Constructeurs
	////////////////////

	public ArbreClause(ArrayList<ArrayList<Formule>> autres) {
		this.formule = null;
		this.autres = autres;
		this.pere = null;
		sousNoeud = new ArrayList<ArbreClause>();
	}

	public ArbreClause(ArrayList<ArrayList<Formule>> autres, ArbreClause pere) {
		this.formule = null;
		this.autres = autres;
		this.pere = pere;
		sousNoeud = new ArrayList<ArbreClause>();
	}

	public ArbreClause(ArrayList<ArrayList<Formule>> autres, ArbreClause pere, ArrayList<Formule> formule) {
		this.formule = formule;
		this.autres = autres;
		this.pere = pere;
		sousNoeud = new ArrayList<ArbreClause>();
	}

	public ArbreClause(ArrayList<ArrayList<Formule>> autres, ArrayList<Formule> formule) {
		this.formule = formule;
		this.autres = autres;
		pere = null;
		sousNoeud = new ArrayList<ArbreClause>();
	}

	/**
	 * Getter permettant de savoir le sous noeud
	 * 
	 * @return l'ArrayList<ArbreClause> sous noeud
	 */
	public ArrayList<ArbreClause> getSousNoeud() {
		return sousNoeud;
	}

	public boolean contientAilleurs(ArrayList<Formule> f) {
		if (pere != null) {

			return pere.contientAilleurs(f);
		} else {

			return contient(f);
		}
	}

	/**
	 * si la clause est contenu dans l'arbre
	 * @param f
	 * @return
	 */
	public boolean contient(ArrayList<Formule> f) {

		if (Resolution.theSame(formule, f)) {

			return true;
		}

		for (ArbreClause fils : sousNoeud) {

			if (fils.contient(f)) {
				return true;
			}
		}

		return false;
	}

	public boolean resoudre() {
		for (int i = 0; i < autres.size(); i++) {
			if (formule.size() == 0) {
				return true;
			}
			// A ou non A
			if (Resolution.theSameNegative(formule, autres.get(i))) {
				return true;
			}

			for (int l = 0; l < formule.size(); l++) {

				for (int m = 0; m < autres.get(i).size(); m++) {
					ArrayList<Formule> ftemp2 = null;
					//unification des deux clauses si possible
					if ((formule.get(l) instanceof Atome && autres.get(i).get(m) instanceof Non) || (formule.get(l) instanceof Non && autres.get(i).get(m) instanceof Atome)) {

						ftemp2 = Resolution.substituer(Resolution.copy(formule), Resolution.copy(autres.get(i)), (Atome) (formule.get(l) instanceof Atome ? (Atome) formule.get(l) : (Atome) ((Non) formule.get(l)).getOperande()).copy(), (Atome) (autres.get(i).get(m) instanceof Atome ? (Atome) autres.get(i).get(m) : (Atome) ((Non) autres.get(i).get(m)).getOperande()).copy());
					}
					if (ftemp2 != null) {

						//si c'est deja contenu ailleurs alors on rrete car la possibilite a deja ete essaye 
						if (!contientAilleurs(ftemp2)) {
							/*
							 * System.out.println("--------Avant unif");
							 * System.out.println(formule);
							 * System.out.println(autres.get(i));
							 * System.out.println("------apres unif");
							 * System.out.println(ftemp2 + "pere "+ formule);
							 */
							//ajout du fils
							ArbreClause fils = new ArbreClause(autres, this, ftemp2);
							this.sousNoeud.add(fils);
							//resolution du fils
							if (fils.resoudre()) {
								return true;
							}

							break;
						} else {

						}

					}
				}

			}
		}

		return false;
	}

	public String toString() {
		String ret = "";
		ret += formule;
		for (ArbreClause ss : sousNoeud) {
			ret += "\n \t" + ss + "avec pere + " + (pere != null ? pere.formule : "");
		}

		return ret;
	}

}
